YES 0.406 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule Monad
  ((mzero :: [a]) :: [a])

module Monad where
  import qualified Maybe
import qualified Prelude
  class Monad a => MonadPlus a where 
    mzero :: MonadPlus a => a b

  instance MonadPlus Maybe where 

instance MonadPlus [] where 
   
mzero = []


module Maybe where
  import qualified Monad
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Monad
  ((mzero :: [a]) :: [a])

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  class Monad a => MonadPlus a where 
    mzero :: MonadPlus a => a b

  instance MonadPlus Maybe where 

instance MonadPlus [] where 
   
mzero = []



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow

mainModule Monad
  (mzero :: [a])

module Monad where
  import qualified Maybe
import qualified Prelude
  class Monad a => MonadPlus a where 
    mzero :: MonadPlus a => a b

  instance MonadPlus Maybe where 

instance MonadPlus [] where 
   
mzero = []


module Maybe where
  import qualified Monad
import qualified Prelude


Haskell To QDPs